\section{Conclusion}\label{sec:conc}
This paper develops improvements to algorithms for backbones extraction.
It's devises new preprocessing techniques for backbones extraction by computing under-approximation of backbones and non-backbones.
In addition, the paper implemented FCB and compared with CB with formulae from MCSes extraction, practical applications and 4 groups of formulae with a fixed percentage of backbones.

The experimental results indicate that FCB is able to reduce the SAT calls number as well as shorten the CPU time cost by a single SAT call.
However, for some of the formulae, CB needs less SAT calls than FCB does, which opening a possibility for portfolio-based solvers.
In other words, a suitable model will reduce the SAT calls number for both CB and FCB.

In the future, we plan to explore more practical applications for backbones, such as hardware model checking, SAT model counting and SAT model enumeration.
